|
| 1: |
|
a__app(nil,YS) |
→ mark(YS) |
| 2: |
|
a__app(cons(X,XS),YS) |
→ cons(mark(X),app(XS,YS)) |
| 3: |
|
a__from(X) |
→ cons(mark(X),from(s(X))) |
| 4: |
|
a__zWadr(nil,YS) |
→ nil |
| 5: |
|
a__zWadr(XS,nil) |
→ nil |
| 6: |
|
a__zWadr(cons(X,XS),cons(Y,YS)) |
→ cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS)) |
| 7: |
|
a__prefix(L) |
→ cons(nil,zWadr(L,prefix(L))) |
| 8: |
|
mark(app(X1,X2)) |
→ a__app(mark(X1),mark(X2)) |
| 9: |
|
mark(from(X)) |
→ a__from(mark(X)) |
| 10: |
|
mark(zWadr(X1,X2)) |
→ a__zWadr(mark(X1),mark(X2)) |
| 11: |
|
mark(prefix(X)) |
→ a__prefix(mark(X)) |
| 12: |
|
mark(nil) |
→ nil |
| 13: |
|
mark(cons(X1,X2)) |
→ cons(mark(X1),X2) |
| 14: |
|
mark(s(X)) |
→ s(mark(X)) |
| 15: |
|
a__app(X1,X2) |
→ app(X1,X2) |
| 16: |
|
a__from(X) |
→ from(X) |
| 17: |
|
a__zWadr(X1,X2) |
→ zWadr(X1,X2) |
| 18: |
|
a__prefix(X) |
→ prefix(X) |
|
There are 18 dependency pairs:
|
| 19: |
|
A__APP(nil,YS) |
→ MARK(YS) |
| 20: |
|
A__APP(cons(X,XS),YS) |
→ MARK(X) |
| 21: |
|
A__FROM(X) |
→ MARK(X) |
| 22: |
|
A__ZWADR(cons(X,XS),cons(Y,YS)) |
→ A__APP(mark(Y),cons(mark(X),nil)) |
| 23: |
|
A__ZWADR(cons(X,XS),cons(Y,YS)) |
→ MARK(Y) |
| 24: |
|
A__ZWADR(cons(X,XS),cons(Y,YS)) |
→ MARK(X) |
| 25: |
|
MARK(app(X1,X2)) |
→ A__APP(mark(X1),mark(X2)) |
| 26: |
|
MARK(app(X1,X2)) |
→ MARK(X1) |
| 27: |
|
MARK(app(X1,X2)) |
→ MARK(X2) |
| 28: |
|
MARK(from(X)) |
→ A__FROM(mark(X)) |
| 29: |
|
MARK(from(X)) |
→ MARK(X) |
| 30: |
|
MARK(zWadr(X1,X2)) |
→ A__ZWADR(mark(X1),mark(X2)) |
| 31: |
|
MARK(zWadr(X1,X2)) |
→ MARK(X1) |
| 32: |
|
MARK(zWadr(X1,X2)) |
→ MARK(X2) |
| 33: |
|
MARK(prefix(X)) |
→ A__PREFIX(mark(X)) |
| 34: |
|
MARK(prefix(X)) |
→ MARK(X) |
| 35: |
|
MARK(cons(X1,X2)) |
→ MARK(X1) |
| 36: |
|
MARK(s(X)) |
→ MARK(X) |
|
The approximated dependency graph contains one SCC:
{19-32,34-36}.